Nuprl Lemma : rel_exp_functionality_wrt_rel_implies
11,40
postcript
pdf
n
:
,
T
:Type,
R1
,
R2
:(
T
T
).
R1
=>
R2
rel_exp(
T
;
R1
;
n
) => rel_exp(
T
;
R2
;
n
)
latex
Definitions
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
Lemmas
rel
exp
monotone
origin
n:
, T:Type, R1, R2:(T
T
). R1 => R2 
rel_exp(T;R1;n) => rel_exp(T;R2;n) n:, T:Type, R1, R2:(TT). R1 => R2 rel_exp(T;R1;n) => rel_exp(T;R2;n) B(x)x:A. B(x)